Nuprl Lemma : box!_wf
0,22
postcript
pdf
B
:Type,
P
:(
B
Prop). []!
P
(
B
Type)
Prop
latex
Definitions
t
T
,
Prop
,
P
Q
,
x
:
A
.
B
(
x
)
,
x
:
A
.
B
(
x
)
,
P
&
Q
,
[]!
P
origin
B:Type, P:(B
Prop). []!P 
(BType)Prop B:Type, P:(BProp). []!P (BType)Prop T
Qx:A. B(x)
x:A. B(x)